Nuprl Definition : ma-init-const
11,40
postcript
pdf
ma-init-const(
M
;
x
) ==
v
!= (
M
.2.2).1(
x
)
constant_function(
v
;
;
M
.ds(
x
))
latex
clarification:
ma-init-const(
M
;
x
) == fpf-val(IdDeq; ((
M
.2.2).1);
x
;
a
,
v
.constant_function(
v
;
;
M
.ds(
x
)))
latex
Definitions
z
!=
f
(
x
)
P
(
a
;
z
)
,
IdDeq
,
t
.1
,
t
.2
,
constant_function(
f
;
A
;
B
)
,
,
M
.ds(
x
)
FDL editor aliases
ma-init-const
origin
constant_function(v;
;M.ds(x))
;M.ds(x))) constant_function(v;;M.ds(x))
;M.ds(x))) P(a;z)